i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
es:event_system{i:l}, l:IdLnk.
(source(l) = i)  (ecl-mng-sends{i:l}(es; i; ds; da; A; l; snd)  prop{i:l}) 

latex

Definitions

suptype(S; T), subtype(S; T), ma-valtype(da; k), decl-state(ds), , es-state(es; i), x. t(x), P  Q, P  Q, t.2, t.1, ecl-mng-sends{i:l}(es; i; ds; da; x; l; snd), prop{i:l}, t  T, P  Q, x:A. B(x), msg-item(ds; da; k; l), x(s), guard(T), P  Q, msg-spec(ds; da)

Lemmas

Knd wf, fpf wf, ecl wf, msg-spec wf, event system wf, IdLnk wf, lsrc wf, Id wf, es-kind wf, es-tag wf, l member wf, es-lnk wf, es-E wf, top wf, id-deq wf, es-vartype wf, es-state-subtype, ma-valtype wf, decl-state wf, le wf, pi2 wf, es-loc-init, es-init wf, es-isrcv wf, assert wf, es-bact wf, mapfilter wf, es-val wf, es-state-when wf, rcv wf, Kind-deq wf, fpf-cap wf, es-valtype wf, es-loc wf, es-state wf, tagged-list-messages wf, ecl-tags wf, es-sends-iff wf, es-decls-iff, es-decls wf